(set-logic QF_NIA)
(set-option :model_validate true)
(set-option :model true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(declare-const i7 Int)
(declare-const i8 Int)
(declare-const i9 Int)
(declare-const i10 Int)
(declare-const i11 Int)
(declare-const i15 Int)
(declare-const i16 Int)
(declare-const i18 Int)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(assert-soft (=> (and v0 (=> v9 (not v4)) v6 (not v4)) (not v4)))
(assert v9)
(assert-soft (or v0 v1 v7 v15 v3 v3 v9 (=> v9 (not v4)) (distinct (= v8 v1 v9 v13 v9) (distinct 11 42) v4 v3 v14 v0 (< 692 i4) v1 v0 v0 v4) v8 v13))
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert v14)
(declare-const v18 Bool)
(assert (or v0 v1 v7 v15 v3 v3 v9 (=> v9 (not v4)) (distinct (= v8 v1 v9 v13 v9) (distinct 11 42) v4 v3 v14 v0 (< 692 i4) v1 v0 v0 v4) v8 v13))
(declare-const v19 Bool)
(declare-const i19 Int)
(assert (or (not v13) (distinct (abs i11) i18)))
(check-sat)
(exit)
